Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
top1(free(x),y) |
→ top2(check(new(x)),y) |
| 2: |
|
top1(free(x),y) |
→ top2(new(x),check(y)) |
| 3: |
|
top1(free(x),y) |
→ top2(check(x),new(y)) |
| 4: |
|
top1(free(x),y) |
→ top2(x,check(new(y))) |
| 5: |
|
top2(x,free(y)) |
→ top1(check(new(x)),y) |
| 6: |
|
top2(x,free(y)) |
→ top1(new(x),check(y)) |
| 7: |
|
top2(x,free(y)) |
→ top1(check(x),new(y)) |
| 8: |
|
top2(x,free(y)) |
→ top1(x,check(new(y))) |
| 9: |
|
new(free(x)) |
→ free(new(x)) |
| 10: |
|
old(free(x)) |
→ free(old(x)) |
| 11: |
|
new(serve) |
→ free(serve) |
| 12: |
|
old(serve) |
→ free(serve) |
| 13: |
|
check(free(x)) |
→ free(check(x)) |
| 14: |
|
check(new(x)) |
→ new(check(x)) |
| 15: |
|
check(old(x)) |
→ old(check(x)) |
| 16: |
|
check(old(x)) |
→ old(x) |
|
There are 27 dependency pairs:
|
| 17: |
|
TOP1(free(x),y) |
→ TOP2(check(new(x)),y) |
| 18: |
|
TOP1(free(x),y) |
→ CHECK(new(x)) |
| 19: |
|
TOP1(free(x),y) |
→ TOP2(new(x),check(y)) |
| 20: |
|
TOP1(free(x),y) |
→ NEW(x) |
| 21: |
|
TOP1(free(x),y) |
→ CHECK(y) |
| 22: |
|
TOP1(free(x),y) |
→ TOP2(check(x),new(y)) |
| 23: |
|
TOP1(free(x),y) |
→ CHECK(x) |
| 24: |
|
TOP1(free(x),y) |
→ TOP2(x,check(new(y))) |
| 25: |
|
TOP1(free(x),y) |
→ CHECK(new(y)) |
| 26: |
|
TOP1(free(x),y) |
→ NEW(y) |
| 27: |
|
TOP2(x,free(y)) |
→ TOP1(check(new(x)),y) |
| 28: |
|
TOP2(x,free(y)) |
→ CHECK(new(x)) |
| 29: |
|
TOP2(x,free(y)) |
→ TOP1(new(x),check(y)) |
| 30: |
|
TOP2(x,free(y)) |
→ NEW(x) |
| 31: |
|
TOP2(x,free(y)) |
→ CHECK(y) |
| 32: |
|
TOP2(x,free(y)) |
→ TOP1(check(x),new(y)) |
| 33: |
|
TOP2(x,free(y)) |
→ CHECK(x) |
| 34: |
|
TOP2(x,free(y)) |
→ TOP1(x,check(new(y))) |
| 35: |
|
TOP2(x,free(y)) |
→ CHECK(new(y)) |
| 36: |
|
TOP2(x,free(y)) |
→ NEW(y) |
| 37: |
|
NEW(free(x)) |
→ NEW(x) |
| 38: |
|
OLD(free(x)) |
→ OLD(x) |
| 39: |
|
CHECK(free(x)) |
→ CHECK(x) |
| 40: |
|
CHECK(new(x)) |
→ NEW(check(x)) |
| 41: |
|
CHECK(new(x)) |
→ CHECK(x) |
| 42: |
|
CHECK(old(x)) |
→ OLD(check(x)) |
| 43: |
|
CHECK(old(x)) |
→ CHECK(x) |
|
The approximated dependency graph contains 4 SCCs:
{37},
{38},
{39,41,43}
and {17,19,22,24,27,29,32,34}.
-
Consider the SCC {37}.
There are no usable rules.
By taking the AF π with
π(NEW) = 1 together with
the lexicographic path order with
empty precedence,
rule 37
is strictly decreasing.
-
Consider the SCC {38}.
There are no usable rules.
By taking the AF π with
π(OLD) = 1 together with
the lexicographic path order with
empty precedence,
rule 38
is strictly decreasing.
-
Consider the SCC {39,41,43}.
There are no usable rules.
By taking the AF π with
π(CHECK) = π(free) = π(new) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {39,41}
are weakly decreasing and
rule 43
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {39,41}.
By taking the AF π with
π(CHECK) = π(free) = 1 together with
the lexicographic path order with
empty precedence,
rule 39
is weakly decreasing and
rule 41
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {39}.
By taking the AF π with
π(CHECK) = 1 together with
the lexicographic path order with
empty precedence,
rule 39
is strictly decreasing.
-
Consider the SCC {17,19,22,24,27,29,32,34}.
The usable rules are {9-16}.
The constraints could not be solved.
Tyrolean Termination Tool (0.49 seconds)
--- May 3, 2006